package com.Clause.Biais;

import java.util.HashSet;
import java.util.Set;

import com.Clause.*;

public class Biais {

	public static void enleverDoubleNegations(Clause clause){
		enleverDoubleNegations(clause.getRoot());
	}

	public static void enleverImplique(Clause clause){
		enleverImplique(clause.getRoot());
	}

	public static void enleverParentheses(Clause clause){
		enleverDoubleNegations(clause);
		enleverParentheses(clause.getRoot());
		enleverDoubleNegations(clause);
	}

	private static void enleverDoubleNegations(ClauseProxy proxy){

		if(proxy != null){
			ClauseElement element = proxy.getElement();

			if(element.getClass().equals(OperateurBinaire.class)){
				OperateurBinaire opbin = (OperateurBinaire)element;
				enleverDoubleNegations(opbin.getPrecedent());
			}
			else{
				if(element.getClass().equals(OperateurUnaire.class)){
					if(((OperateurUnaire)element).getOperateur().equals(OperateurUnaire.NOT)){     //si element = NOT

						boolean finit = false;

						ClauseElement aux = ((OperateurUnaire)element);

						while(!finit){
							finit = true;
							if(aux.getSuivant() != null)
								if(aux.getElementSuivant().getClass().equals(OperateurUnaire.class) &&
										(((OperateurUnaire)aux.getElementSuivant()).getOperateur().equals(OperateurUnaire.NOT))){  //si on a un deuxieme NOT
									OperateurUnaire opu_aux = (OperateurUnaire)aux.getElementSuivant();
									if(opu_aux.getOperateur().equals(OperateurUnaire.NOT)){
										aux = opu_aux.getElementSuivant();
										finit = false;
									}
								}
						}

						proxy.setElement(aux);
					}
				}
			}
			enleverDoubleNegations(proxy.getSuivant());
		}
	}

	private static void enleverImplique(ClauseProxy proxy){
		if(proxy.getElement().getClass().equals(OperateurBinaire.class)){
			OperateurBinaire opbin = (OperateurBinaire)proxy.getElement();
			if(opbin.getOperateur().equals(OperateurBinaire.IMPLIQUE)){
				OperateurUnaire not = OperateurUnaire.newNot(opbin.getElementPrecedent());
				opbin.setElementPrecedent(not);
				opbin.changer(OperateurBinaire.OU);
			}
			else{
				enleverImplique(opbin.getPrecedent());
				enleverImplique(opbin.getSuivant());
			}
		}
		else
			enleverImplique(proxy.getSuivant());
	}

	private static void distribuerNot(ClauseProxy proxy){ //proxy est négatif
		if(proxy != null && proxy.getElement().getSuivant() != null){
			ClauseElement elementSuivant = proxy.getElement().getElementSuivant();

			if(elementSuivant.getClass().equals(Parenthese.class)){ //si le ! est suivi d'une parenthese
				//il est donc suivi d'un operateur binaire

				ClauseElement elementSuivant2 = elementSuivant.getElementSuivant();

				if(elementSuivant2.getClass().equals(OperateurBinaire.class)){ //operateur binaire
					OperateurBinaire opbin2 = (OperateurBinaire)elementSuivant2;
					opbin2.interchanger();

					OperateurUnaire not1 = OperateurUnaire.newNot(opbin2.getElementPrecedent());
					OperateurUnaire not2 = OperateurUnaire.newNot(opbin2.getElementSuivant());

					opbin2.setElementPrecedent(not1);
					opbin2.setElementSuivant(not2);

					distribuerNot(opbin2.getPrecedent());
					distribuerNot(opbin2.getSuivant());
				}
				
				if(elementSuivant2.getClass().equals(OperateurUnaire.class)){					
					elementSuivant.setElementSuivant(elementSuivant2.getElementSuivant());

					distribuerNot(elementSuivant.getSuivant());
				}

				proxy.setElement(elementSuivant);
				enleverParentheses(proxy);

			}
		}
	}
	
	public static void toImplique(ClauseProxy proxy){
		if(proxy != null){
			enleverParentheses(proxy);
			enleverDoubleNegations(proxy);
			
			ClauseElement element = proxy.getElement();
			if(element.getClass().equals(OperateurBinaire.class)){
				OperateurBinaire opbin = (OperateurBinaire)element;
				if(opbin.getOperateur().equals(OperateurBinaire.OU)){
					opbin.changer(OperateurBinaire.IMPLIQUE);
					
					OperateurUnaire not = OperateurUnaire.newNot(new Parenthese(opbin.getElementPrecedent()));

					opbin.setElementPrecedent(not);
					distribuerNot(proxy);
					enleverParentheses(proxy);
					enleverDoubleNegations(proxy);
										
				}
			}
			else if(element.getClass().equals(OperateurUnaire.class) && 
					((OperateurUnaire)element).getOperateur().equals(OperateurUnaire.NOT)){
				distribuerNot(proxy);
			}
		}
	}

	public static void enleverParentheses(ClauseProxy proxy) {
		if(proxy != null){
			ClauseElement element = proxy.getElement();
			if(element.getClass().equals(Parenthese.class)){ //si c'est une parenthese
				proxy.setElement(proxy.getSuivant()); //on enleve la parenthese
				enleverParentheses(proxy.getSuivant());
			}
			else if(element.getClass().equals(OperateurBinaire.class)){
				enleverParentheses(proxy.getSuivant());
				enleverParentheses(((OperateurBinaire)element).getPrecedent());
			}
			else if(element.getClass().equals(OperateurUnaire.class) && 
					((OperateurUnaire)element).getOperateur().equals(OperateurUnaire.NOT)){
				distribuerNot(proxy);
			}
		}
	}

	public static int compter(ClauseProxy proxy, String nom_class){

		int nombre = 0;

		if(proxy.getElement().getClass().toString().equals(nom_class)){
			nombre = 1;
		}

		if(proxy.getElement().getClass().equals(OperateurBinaire.class)){
			OperateurBinaire opbin = (OperateurBinaire) proxy.getElement();
			return nombre + 
					compter(opbin.getPrecedent(),nom_class) +
					compter(opbin.getSuivant(),nom_class);
		}
		else if(proxy.getElement().getClass().equals(OperateurUnaire.class) || 
				proxy.getElement().getClass().equals(Parenthese.class)){
			return nombre + compter(proxy.getSuivant(),nom_class);
		}
		else if(proxy.getElement().getClass().equals(Predicat.class) || 
				proxy.getElement().getClass().equals(Variable.class)){
			return nombre;
		}

		return nombre; //jamais atteint
	}

	public static HashSet<ClauseElement> get(ClauseProxy proxy, String nom_class){
		HashSet<ClauseElement> elements = new HashSet<ClauseElement>();
		get(proxy,nom_class,elements);
		return elements;
	}

	private static void get(ClauseProxy proxy, String nom_class,Set<ClauseElement> elements){
		if(proxy.getElement().getClass().toString().equals(nom_class)){
			elements.add(proxy.getElement());
		}

		if(proxy.getElement().getClass().equals(OperateurBinaire.class)){
			OperateurBinaire opbin = (OperateurBinaire) proxy.getElement();
			get(opbin.getPrecedent(),nom_class,elements);
			get(opbin.getSuivant(),nom_class,elements);
		}
		else if(proxy.getElement().getClass().equals(OperateurUnaire.class) || 
				proxy.getElement().getClass().equals(Parenthese.class)){
			get(proxy.getSuivant(),nom_class,elements);
		}
		else if(proxy.getElement().getClass().equals(Predicat.class)) {
			Predicat p = (Predicat) proxy.getElement();
			for(Variable v : p.getVariable()){
				get(new ClauseProxy(v),nom_class,elements);
			}
		}
	}

	public static void toImplique(Clause clause) {
		toImplique(clause.getRoot());
	}

}
